* Step 1: DependencyPairs WORST_CASE(?,O(1))
+ Considered Problem:
- Strict TRS:
a(c(d(x))) -> c(x)
u(b(d(d(x)))) -> b(x)
v(c(x)) -> b(x)
w(c(x)) -> b(x)
- Signature:
{a/1,u/1,v/1,w/1} / {b/1,c/1,d/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {a,u,v,w} and constructors {b,c,d}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
a#(c(d(x))) -> c_1()
u#(b(d(d(x)))) -> c_2()
v#(c(x)) -> c_3()
w#(c(x)) -> c_4()
Weak DPs
and mark the set of starting terms.
* Step 2: UsableRules WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
a#(c(d(x))) -> c_1()
u#(b(d(d(x)))) -> c_2()
v#(c(x)) -> c_3()
w#(c(x)) -> c_4()
- Weak TRS:
a(c(d(x))) -> c(x)
u(b(d(d(x)))) -> b(x)
v(c(x)) -> b(x)
w(c(x)) -> b(x)
- Signature:
{a/1,u/1,v/1,w/1,a#/1,u#/1,v#/1,w#/1} / {b/1,c/1,d/1,c_1/0,c_2/0,c_3/0,c_4/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {a#,u#,v#,w#} and constructors {b,c,d}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
a#(c(d(x))) -> c_1()
u#(b(d(d(x)))) -> c_2()
v#(c(x)) -> c_3()
w#(c(x)) -> c_4()
* Step 3: Trivial WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
a#(c(d(x))) -> c_1()
u#(b(d(d(x)))) -> c_2()
v#(c(x)) -> c_3()
w#(c(x)) -> c_4()
- Signature:
{a/1,u/1,v/1,w/1,a#/1,u#/1,v#/1,w#/1} / {b/1,c/1,d/1,c_1/0,c_2/0,c_3/0,c_4/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {a#,u#,v#,w#} and constructors {b,c,d}
+ Applied Processor:
Trivial
+ Details:
Consider the dependency graph
1:S:a#(c(d(x))) -> c_1()
2:S:u#(b(d(d(x)))) -> c_2()
3:S:v#(c(x)) -> c_3()
4:S:w#(c(x)) -> c_4()
The dependency graph contains no loops, we remove all dependency pairs.
* Step 4: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Signature:
{a/1,u/1,v/1,w/1,a#/1,u#/1,v#/1,w#/1} / {b/1,c/1,d/1,c_1/0,c_2/0,c_3/0,c_4/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {a#,u#,v#,w#} and constructors {b,c,d}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(1))